COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	Proof? 
C00015 ENDMK
C⊗;
Proof? 
;;; permut.lsp[f82,jmc]	ekl axioms and proofs for permutation functions

(get-proofs lispax)
(proof permut)

(decl rac (unaryname: rac) (type: |ground→ground|) (syntype: constant)
 (bindingpower: 950))
 
(decl rdc (unaryname: rdc) (type: |ground→ground|) (syntype: constant)
 (bindingpower: 950))

(decl snoc (type: |(ground⊗ground)→ground|) (syntype: constant))

(axiom |∀u.rdc u = if null cdr u then nil else car u . rdc cdr u|)
(label definfo)

(axiom |∀u.rac u = if null cdr u then car u else rac cdr u|)
(label definfo)

(axiom |∀x u.snoc(x,u) = u * x.nil|)
(label definfo)
(label snoc_def)

(decl reverse (unaryname: reverse) (type: |ground→ground|) (syntype: constant)
 (bindingpower: 950))

(decl rev (type: |ground⊗ground→ground|) (syntype: constant))

(axiom |∀u.reverse = rev(u,nil)|)
(label reverse_rev)

(axiom |∀u v.rev(u,v) = if null u then v else rev(cdr u, car u . v)|)
(label definfo)

(axiom |∀u.reverse u = if null u then nil else reverse cdr u * car u . nil|)
(label reverse_def)
(label definfo)

(axiom |∀u.listp reverse u|)
(label sortinfo)

(axiom |∀u.reverse reverse u = u|)
(label simpinfo)
(label reverse_reverse)

(axiom |∀u v.reverse(u*v) = reverse v * reverse u|)
(label reverse_append)

(decl lcycle (unaryname: lcycle) (type: |ground→ground|) (syntype: constant)
 (bindingpower: 950))

(decl rcycle (unaryname: rcycle) (type: |ground→ground|) (syntype: constant)
 (bindingpower: 950))

(axiom |∀u.lcycle u = if null u then nil else snoc(cdr u, car u)|)
(label definfo)

(axiom |∀u.rcycle u = if null u then nil else rac u . rdc u|)
(label definfo)

;end_defs

(trw |reverse(x.nil)| (use reverse_def (mode: t)) sortinfo simpinfo reverse_def)

(TRW |REVERSE SNOC(X,U)|
      ((USE SNOC_DEF (MODE: T)) (USE (REVERSE_APPEND SORTINFO) (MODE: T))
        (USE 19)) SORTINFO)

(rw 20 (use append_def (mode: t)) sortinfo simpinfo)
REVERSE (X.NIL)=X.NIL

20. REVERSE SNOC(X,U)=X.NIL*REVERSE U

21. REVERSE SNOC(X,U)=X.REVERSE U

22. 

(TRW |REVERSE SNOC(X,U)|
      ((USE SNOC_DEF (MODE: T)) (USE (REVERSE_APPEND SORTINFO) (MODE: T))
        (USE 19)
	(use (append_def sortinfo simpinfo) (mode: t))
) SORTINFO)
REVERSE SNOC(X,U)=(IF NULL U THEN X.NIL ELSE REVERSE (CAR U.(CDR U*X.NIL)))

(deletel)
;Done.
(derive |reverse reverse snoc(x,u) = reverse (x.reverse u)| 21)
; failed to derive 
REVERSE (REVERSE (X.U))=REVERSE (X.REVERSE U)

(rw 22 (use reverse_reverse) sortinfo)
(deletel)

23. ;Done.
22. REVERSE (REVERSE SNOC(X,U))=REVERSE (X.REVERSE U)

23. REVERSE (REVERSE SNOC(X,U))=REVERSE (X.REVERSE U)

(save-proofs permut)
;Done.
23. ;Done.
23.